x,y:atom{2:n}. (eq_atom{2:n}(x; y))  (x = y) 

latex

Definitions	eq_atom{$n:n}(x; y), prop{i:l}, t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), False, A, P  Q, decidable(P)
Lemmas	btrue wf, eqtt to assert, assert of bnot, bfalse wf, eqff to assert, decidable atom equal 2, eq atom wf2, assert wf